The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS
↳1 DependencyGraphProof (BOTH BOUNDS(ID, ID), 17 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳6 CdtProblem
↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 CdtUsableRulesProof (⇔, 0 ms)
↳10 CdtProblem
↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 82 ms)
↳12 CdtProblem
↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 0 ms)
↳14 CdtProblem
↳15 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

pairNs → cons(0, n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Rewrite Strategy: INNERMOST

(1) DependencyGraphProof (BOTH BOUNDS(ID, ID) transformation)

The following rules are not reachable from basic terms in the dependency graph and can be removed:
tail(cons(X, XS)) → activate(XS)

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

zip(nil, XS) → nil
zip(X, nil) → nil
repItems(X) → n__repItems(X)
activate(n__repItems(X)) → repItems(activate(X))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
activate(X) → X
activate(n__incr(X)) → incr(activate(X))
cons(X1, X2) → n__cons(X1, X2)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
incr(X) → n__incr(X)
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
repItems(nil) → nil
take(0, XS) → nil
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__oddNs) → oddNs
pairNs → cons(0, n__incr(n__oddNs))
oddNs → incr(pairNs)
zip(X1, X2) → n__zip(X1, X2)
activate(n__cons(X1, X2)) → cons(activate(X1), X2)

Rewrite Strategy: INNERMOST

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

zip(nil, z0) → nil
zip(z0, nil) → nil
zip(cons(z0, z1), cons(z2, z3)) → cons(pair(z0, z2), n__zip(activate(z1), activate(z3)))
zip(z0, z1) → n__zip(z0, z1)
repItems(z0) → n__repItems(z0)
repItems(cons(z0, z1)) → cons(z0, n__cons(z0, n__repItems(activate(z1))))
repItems(nil) → nil
activate(n__repItems(z0)) → repItems(activate(z0))
activate(z0) → z0
activate(n__incr(z0)) → incr(activate(z0))
activate(n__zip(z0, z1)) → zip(activate(z0), activate(z1))
activate(n__take(z0, z1)) → take(activate(z0), activate(z1))
activate(n__oddNs) → oddNs
activate(n__cons(z0, z1)) → cons(activate(z0), z1)
take(s(z0), cons(z1, z2)) → cons(z1, n__take(z0, activate(z2)))
take(z0, z1) → n__take(z0, z1)
take(0, z0) → nil
cons(z0, z1) → n__cons(z0, z1)
incr(cons(z0, z1)) → cons(s(z0), n__incr(activate(z1)))
incr(z0) → n__incr(z0)
oddNs → n__oddNs
oddNs → incr(pairNs)
pairNs → cons(0, n__incr(n__oddNs))
Tuples:

ZIP(nil, z0) → c
ZIP(z0, nil) → c1
ZIP(cons(z0, z1), cons(z2, z3)) → c2(CONS(pair(z0, z2), n__zip(activate(z1), activate(z3))), ACTIVATE(z1), ACTIVATE(z3))
ZIP(z0, z1) → c3
REPITEMS(z0) → c4
REPITEMS(cons(z0, z1)) → c5(CONS(z0, n__cons(z0, n__repItems(activate(z1)))), ACTIVATE(z1))
REPITEMS(nil) → c6
ACTIVATE(n__repItems(z0)) → c7(REPITEMS(activate(z0)), ACTIVATE(z0))
ACTIVATE(z0) → c8
ACTIVATE(n__incr(z0)) → c9(INCR(activate(z0)), ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ZIP(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(TAKE(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__oddNs) → c12(ODDNS)
ACTIVATE(n__cons(z0, z1)) → c13(CONS(activate(z0), z1), ACTIVATE(z0))
TAKE(s(z0), cons(z1, z2)) → c14(CONS(z1, n__take(z0, activate(z2))), ACTIVATE(z2))
TAKE(z0, z1) → c15
TAKE(0, z0) → c16
CONS(z0, z1) → c17
INCR(cons(z0, z1)) → c18(CONS(s(z0), n__incr(activate(z1))), ACTIVATE(z1))
INCR(z0) → c19
ODDNS → c20
ODDNS → c21(INCR(pairNs), PAIRNS)
PAIRNS → c22(CONS(0, n__incr(n__oddNs)))
S tuples:

ZIP(nil, z0) → c
ZIP(z0, nil) → c1
ZIP(cons(z0, z1), cons(z2, z3)) → c2(CONS(pair(z0, z2), n__zip(activate(z1), activate(z3))), ACTIVATE(z1), ACTIVATE(z3))
ZIP(z0, z1) → c3
REPITEMS(z0) → c4
REPITEMS(cons(z0, z1)) → c5(CONS(z0, n__cons(z0, n__repItems(activate(z1)))), ACTIVATE(z1))
REPITEMS(nil) → c6
ACTIVATE(n__repItems(z0)) → c7(REPITEMS(activate(z0)), ACTIVATE(z0))
ACTIVATE(z0) → c8
ACTIVATE(n__incr(z0)) → c9(INCR(activate(z0)), ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ZIP(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(TAKE(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__oddNs) → c12(ODDNS)
ACTIVATE(n__cons(z0, z1)) → c13(CONS(activate(z0), z1), ACTIVATE(z0))
TAKE(s(z0), cons(z1, z2)) → c14(CONS(z1, n__take(z0, activate(z2))), ACTIVATE(z2))
TAKE(z0, z1) → c15
TAKE(0, z0) → c16
CONS(z0, z1) → c17
INCR(cons(z0, z1)) → c18(CONS(s(z0), n__incr(activate(z1))), ACTIVATE(z1))
INCR(z0) → c19
ODDNS → c20
ODDNS → c21(INCR(pairNs), PAIRNS)
PAIRNS → c22(CONS(0, n__incr(n__oddNs)))
K tuples:none
Defined Rule Symbols:

zip, repItems, activate, take, cons, incr, oddNs, pairNs

Defined Pair Symbols:

ZIP, REPITEMS, ACTIVATE, TAKE, CONS, INCR, ODDNS, PAIRNS

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 4 leading nodes:

ZIP(cons(z0, z1), cons(z2, z3)) → c2(CONS(pair(z0, z2), n__zip(activate(z1), activate(z3))), ACTIVATE(z1), ACTIVATE(z3))
REPITEMS(cons(z0, z1)) → c5(CONS(z0, n__cons(z0, n__repItems(activate(z1)))), ACTIVATE(z1))
TAKE(s(z0), cons(z1, z2)) → c14(CONS(z1, n__take(z0, activate(z2))), ACTIVATE(z2))
INCR(cons(z0, z1)) → c18(CONS(s(z0), n__incr(activate(z1))), ACTIVATE(z1))
Removed 14 trailing nodes:

ACTIVATE(n__oddNs) → c12(ODDNS)
PAIRNS → c22(CONS(0, n__incr(n__oddNs)))
TAKE(z0, z1) → c15
ODDNS → c20
TAKE(0, z0) → c16
REPITEMS(nil) → c6
ZIP(z0, nil) → c1
ODDNS → c21(INCR(pairNs), PAIRNS)
REPITEMS(z0) → c4
ZIP(z0, z1) → c3
INCR(z0) → c19
CONS(z0, z1) → c17
ACTIVATE(z0) → c8
ZIP(nil, z0) → c

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

zip(nil, z0) → nil
zip(z0, nil) → nil
zip(cons(z0, z1), cons(z2, z3)) → cons(pair(z0, z2), n__zip(activate(z1), activate(z3)))
zip(z0, z1) → n__zip(z0, z1)
repItems(z0) → n__repItems(z0)
repItems(cons(z0, z1)) → cons(z0, n__cons(z0, n__repItems(activate(z1))))
repItems(nil) → nil
activate(n__repItems(z0)) → repItems(activate(z0))
activate(z0) → z0
activate(n__incr(z0)) → incr(activate(z0))
activate(n__zip(z0, z1)) → zip(activate(z0), activate(z1))
activate(n__take(z0, z1)) → take(activate(z0), activate(z1))
activate(n__oddNs) → oddNs
activate(n__cons(z0, z1)) → cons(activate(z0), z1)
take(s(z0), cons(z1, z2)) → cons(z1, n__take(z0, activate(z2)))
take(z0, z1) → n__take(z0, z1)
take(0, z0) → nil
cons(z0, z1) → n__cons(z0, z1)
incr(cons(z0, z1)) → cons(s(z0), n__incr(activate(z1)))
incr(z0) → n__incr(z0)
oddNs → n__oddNs
oddNs → incr(pairNs)
pairNs → cons(0, n__incr(n__oddNs))
Tuples:

ACTIVATE(n__repItems(z0)) → c7(REPITEMS(activate(z0)), ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(INCR(activate(z0)), ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ZIP(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(TAKE(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(CONS(activate(z0), z1), ACTIVATE(z0))
S tuples:

ACTIVATE(n__repItems(z0)) → c7(REPITEMS(activate(z0)), ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(INCR(activate(z0)), ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ZIP(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(TAKE(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(CONS(activate(z0), z1), ACTIVATE(z0))
K tuples:none
Defined Rule Symbols:

zip, repItems, activate, take, cons, incr, oddNs, pairNs

Defined Pair Symbols:

ACTIVATE

Compound Symbols:

c7, c9, c10, c11, c13

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

zip(nil, z0) → nil
zip(z0, nil) → nil
zip(cons(z0, z1), cons(z2, z3)) → cons(pair(z0, z2), n__zip(activate(z1), activate(z3)))
zip(z0, z1) → n__zip(z0, z1)
repItems(z0) → n__repItems(z0)
repItems(cons(z0, z1)) → cons(z0, n__cons(z0, n__repItems(activate(z1))))
repItems(nil) → nil
activate(n__repItems(z0)) → repItems(activate(z0))
activate(z0) → z0
activate(n__incr(z0)) → incr(activate(z0))
activate(n__zip(z0, z1)) → zip(activate(z0), activate(z1))
activate(n__take(z0, z1)) → take(activate(z0), activate(z1))
activate(n__oddNs) → oddNs
activate(n__cons(z0, z1)) → cons(activate(z0), z1)
take(s(z0), cons(z1, z2)) → cons(z1, n__take(z0, activate(z2)))
take(z0, z1) → n__take(z0, z1)
take(0, z0) → nil
cons(z0, z1) → n__cons(z0, z1)
incr(cons(z0, z1)) → cons(s(z0), n__incr(activate(z1)))
incr(z0) → n__incr(z0)
oddNs → n__oddNs
oddNs → incr(pairNs)
pairNs → cons(0, n__incr(n__oddNs))
Tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
S tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
K tuples:none
Defined Rule Symbols:

zip, repItems, activate, take, cons, incr, oddNs, pairNs

Defined Pair Symbols:

ACTIVATE

Compound Symbols:

c7, c9, c10, c11, c13

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

zip(nil, z0) → nil
zip(z0, nil) → nil
zip(cons(z0, z1), cons(z2, z3)) → cons(pair(z0, z2), n__zip(activate(z1), activate(z3)))
zip(z0, z1) → n__zip(z0, z1)
repItems(z0) → n__repItems(z0)
repItems(cons(z0, z1)) → cons(z0, n__cons(z0, n__repItems(activate(z1))))
repItems(nil) → nil
activate(n__repItems(z0)) → repItems(activate(z0))
activate(z0) → z0
activate(n__incr(z0)) → incr(activate(z0))
activate(n__zip(z0, z1)) → zip(activate(z0), activate(z1))
activate(n__take(z0, z1)) → take(activate(z0), activate(z1))
activate(n__oddNs) → oddNs
activate(n__cons(z0, z1)) → cons(activate(z0), z1)
take(s(z0), cons(z1, z2)) → cons(z1, n__take(z0, activate(z2)))
take(z0, z1) → n__take(z0, z1)
take(0, z0) → nil
cons(z0, z1) → n__cons(z0, z1)
incr(cons(z0, z1)) → cons(s(z0), n__incr(activate(z1)))
incr(z0) → n__incr(z0)
oddNs → n__oddNs
oddNs → incr(pairNs)
pairNs → cons(0, n__incr(n__oddNs))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
S tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

ACTIVATE

Compound Symbols:

c7, c9, c10, c11, c13

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
We considered the (Usable) Rules:none
And the Tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVATE(x1)) = [2]x1   
POL(c10(x1, x2)) = x1 + x2   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c7(x1)) = x1   
POL(c9(x1)) = x1   
POL(n__cons(x1, x2)) = x1   
POL(n__incr(x1)) = [2] + x1   
POL(n__repItems(x1)) = [2] + x1   
POL(n__take(x1, x2)) = [2] + x1 + x2   
POL(n__zip(x1, x2)) = [1] + x1 + x2   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
S tuples:

ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
K tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
Defined Rule Symbols:none

Defined Pair Symbols:

ACTIVATE

Compound Symbols:

c7, c9, c10, c11, c13

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
We considered the (Usable) Rules:none
And the Tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVATE(x1)) = x1   
POL(c10(x1, x2)) = x1 + x2   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1)) = x1   
POL(c7(x1)) = x1   
POL(c9(x1)) = x1   
POL(n__cons(x1, x2)) = [1] + x1   
POL(n__incr(x1)) = x1   
POL(n__repItems(x1)) = x1   
POL(n__take(x1, x2)) = x1 + x2   
POL(n__zip(x1, x2)) = [1] + x1 + x2   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
S tuples:none
K tuples:

ACTIVATE(n__repItems(z0)) → c7(ACTIVATE(z0))
ACTIVATE(n__incr(z0)) → c9(ACTIVATE(z0))
ACTIVATE(n__zip(z0, z1)) → c10(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__take(z0, z1)) → c11(ACTIVATE(z0), ACTIVATE(z1))
ACTIVATE(n__cons(z0, z1)) → c13(ACTIVATE(z0))
Defined Rule Symbols:none

Defined Pair Symbols:

ACTIVATE

Compound Symbols:

c7, c9, c10, c11, c13

(15) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(16) BOUNDS(1, 1)